This invention relates to modifying descriptions of state elements for use in verification of VLSI circuit designs, and in particular for replacing SET/RESET latch ("S/R-Latch") descriptions with DATA latch ("D-Latch") descriptions.
Logic abstraction provides a link between the millions of transistors that comprise a digital VLSI circuit and the high level descriptions used to verify that a circuit implementation matches a set of desired specifications. To verify the logical functionality of a VLSI circuit, designers typically perform both simulation of the circuit implementation and verification of the implementation with respect to the specification. Logic abstraction produces a tractable description of an actual circuit and guarantees that the representation correctly depicts the actual circuit.
State elements, which are devices capable of maintaining an output value independent of their input variables, have presented difficulties for logic abstraction processes. Two types of state elements are typically used in digital MOS design, S/R-Latches and D-Latches. Straightforward, automated techniques exist for abstracting S/R-Latches from circuit implementations.
It is often useful to describe state elements as D-Latches. The SET and RESET expressions required for S/R-Latches are typically two or more times as complex as the expressions required for D-Latches. Moreover, circuit designers often explicitly design state elements as D-Latches. An S/R-Latch description of a state element that was explicitly designed as a D-Latch can confuse the designer and thereby make the verification process more difficult to perform.
One technique for identifying D-Latches is to rely on pattern matching to identify device topologies that are known to implement D-Latches.